0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 84 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 0 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 PiDPToQDPProof (⇔, 0 ms)
↳16 QDP
↳17 QDPSizeChangeProof (⇔, 0 ms)
↳18 YES
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U2_GG(X1, X2, X3, X4, memberB_in_gg(X1, X4))
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → MEMBERB_IN_GG(X1, X4)
MEMBERB_IN_GG(X1, .(X2, X3)) → U1_GG(X1, X2, X3, memberB_in_gg(X1, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → U4_GG(X1, X2, X3, X4, subsetA_in_gg(X2, .(X3, X4)))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → U5_GG(X1, X2, X3, subsetA_in_gg(X2, .(X1, X3)))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))
membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U2_GG(X1, X2, X3, X4, memberB_in_gg(X1, X4))
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → MEMBERB_IN_GG(X1, X4)
MEMBERB_IN_GG(X1, .(X2, X3)) → U1_GG(X1, X2, X3, memberB_in_gg(X1, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → U4_GG(X1, X2, X3, X4, subsetA_in_gg(X2, .(X3, X4)))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → U5_GG(X1, X2, X3, subsetA_in_gg(X2, .(X1, X3)))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))
membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
MEMBERB_IN_GG(X1, .(X2, X3)) → MEMBERB_IN_GG(X1, X3)
From the DPs we obtained the following set of size-change graphs:
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))
membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
SUBSETA_IN_GG(.(X1, X2), .(X3, X4)) → U3_GG(X1, X2, X3, X4, membercB_in_gg(X1, X4))
U3_GG(X1, X2, X3, X4, membercB_out_gg(X1, X4)) → SUBSETA_IN_GG(X2, .(X3, X4))
SUBSETA_IN_GG(.(X1, X2), .(X1, X3)) → SUBSETA_IN_GG(X2, .(X1, X3))
membercB_in_gg(X1, .(X2, X3)) → U10_gg(X1, X2, X3, membercB_in_gg(X1, X3))
membercB_in_gg(X1, .(X1, X2)) → membercB_out_gg(X1, .(X1, X2))
U10_gg(X1, X2, X3, membercB_out_gg(X1, X3)) → membercB_out_gg(X1, .(X2, X3))
membercB_in_gg(x0, x1)
U10_gg(x0, x1, x2, x3)
From the DPs we obtained the following set of size-change graphs: